package arlab.picosat2
import arlab.formulae._
import picosat._
import scala.collection.immutable._
import arlab.formulae.transformations._
object picosatTestObject {
    def main (args: Array[String]) ={
        var s = sat
        
//        s.picosat_reset()
        s.picosat_init()
        
        s.picosat_add(1)
        s.picosat_add(-2)
        s.picosat_add(0) 
                
        s.picosat_add(-1)
        s.picosat_add(2)
        s.picosat_add(0)
        
        println(s.picosat_sat(-1) + " should be 10")

        println(s.picosat_sat(-1))
        println(s.picosat_deref(-1))

        
        s.picosat_add(3)
        s.picosat_add(0)
        
        s.picosat_add(-3)
        s.picosat_add(0)
            
        println(s.picosat_sat(-1) + " should be 20")
        
        val a = Not(And(Or(Or(BooleanVariable("a"),BooleanVariable("b")),Not(BooleanVariable("c"))),Or(Or(Not(BooleanVariable("a")),BooleanVariable("d")),Not(BooleanVariable("g")))))
        println("normal:")
        println(a)        
        println("cnf:")
        println(Transformations.cnf(a))
        println("erfuellbar:")
        s.picosat_reset()
        s.picosat_init()
        println(s.solve(Transformations.cnf(a)))
        
        val b = And(BooleanVariable("a"), Not(BooleanVariable("a")))
        println("normal:")
        println(b)        
        println("cnf:")
        println(Transformations.cnf(b))
        println("erfuellbar:")
        s.picosat_reset()
        s.picosat_init()
        println(s.solve(Transformations.cnf(b)))
      
      
        val c = And(Or(BooleanVariable("a"),BooleanVariable("a")), Or(Not(BooleanVariable("a")),Not(BooleanVariable("a"))))
        println("normal:")
        println(c)        
        println("cnf:")
        println(Transformations.cnf(c))
        println("erfuellbar:")
        s.picosat_reset()
        s.picosat_init()
        println(s.solve(Transformations.cnf(c)))
       
    }
    
}


case object sat extends CPicosat{
    // Bekommt eine Formel in cnf und laesst sie durch picosat loesen.
    // ist die Formel loesbar wird true zurueckgegeben
    def solve(fm:Formula):Boolean = {
 //       println("pars variables into solver")
        addAllVariables(fm)
   //     println("start solver")
        picosat_sat(-1) == 10

 /*       val ret = picosat_sat(-1) == 10
       
        println(
        "x0: " + picosat_deref(getLabel("x0")) +         
        " y0: " + picosat_deref(getLabel("y0")) +         
        " z0: " + picosat_deref(getLabel("z0")))
        
        
        println(
        "x1: " + picosat_deref(getLabel("x1")) +         
        " y1: " + picosat_deref(getLabel("y1")) +         
        " z1: " + picosat_deref(getLabel("z1")))
        
        println(
        "x2: " + picosat_deref(getLabel("x2")) +         
        " y2: " + picosat_deref(getLabel("y2")) +         
        " z2: " + picosat_deref(getLabel("z2")))
        
        
        ret */
      }
    
    //fuegt alle Variablen zu picosat hinzu
    def addAllVariables(fm:Formula):Unit = fm match{
        case BooleanVariable(l) => {
            picosat_add(getLabel(l))
            picosat_add(0)
        }
        case Not(BooleanVariable(l)) => {
            picosat_add(-1 * getLabel(l))
            picosat_add(0)
        }
        case Or(a,b) => {
            addAllVariablesWithout0(a)
            addAllVariablesWithout0(b)
            picosat_add(0)
        }
        case And(a,b) => {
            addAllVariables(a)
            addAllVariables(b)
        }
    }
    //hilfsfunktion
    def addAllVariablesWithout0(fm:Formula):Unit = fm match{
        case BooleanVariable(l) => picosat_add(getLabel(l))
        case Not(BooleanVariable(l)) => picosat_add(-1 * getLabel(l))
        case Or(a,b) => {
            addAllVariablesWithout0(a)
            addAllVariablesWithout0(b)
        }
    }
    
    var hm = new HashMap[String, Integer]
    var max = 0
    //ermittelt einen integer für eine Variable
    def getLabel(l:String):Integer = hm.get(l) match {
        case Some(i) => i
        case other => { max = max+1
                        hm = hm.updated(l,max)
                        max
                      }
    }
    
}
